A:Realizer, ns, ms:(MaName List). ns  ms  A|ns  A|ms 

latex

Definitions

P & Q, True, A, , l_disjoint(T;l1;l2), if p:P then A(p) else B fi , ff, Rplus-right(x1), Rplus-left(x1), Rplus?(x1), if b then t else f fi , Y, if nms1 and nms2 overlap then x else y fi, Rtransform(f;A), x. t(x), t  T, R|names, P  Q, x:A. B(x), xL. P(x), False, P  Q, Dec(P), x(s), Unit, A  B, Realizer, Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), left  right, Rnone(),

Lemmas

R-sub-plus-right2, R-sub-plus-left2, R-sub transitivity, R-plus wf, R-restrict wf, R-plus-sub, es realizer wf, Rrframe wf, Rbframe wf, Raframe wf, Rpre wf, Rsends wf, Reffect wf, Rsframe wf, Rframe wf, R-sub-self, l member wf, Rinit wf, R-names wf, l contains wf, l disjoint wf, decidable wf, MaName wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf